﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.Extensions;
using TruthTree2.PC.Logic;

namespace TruthTree2.PC.Resolution
{
    public class CNFSet
    {
        public List<CNFClause> Clauses;

        public CNFSet()
        {
            Clauses = new List<CNFClause>();
        }
        public CNFSet(List<Sentence> sentences)
        {
            Clauses = new List<CNFClause>();

            CNFSet overall = new CNFSet();
            foreach (Sentence s in sentences)
            {
                Sentence asCNF = s.ConvertToCNFSentence();
                overall = Union(overall, asCNF.ConvertToCNF());
            }

            Clauses.AddRange(overall.Clauses);
        }
        public CNFSet(List<CNFClause> clauses)
        {
            Clauses = clauses;
            if (Clauses == null) { Clauses = new List<CNFClause>(); }
        }

        public static CNFSet Union(CNFSet a, CNFSet b)
        {
            List<CNFClause> cl = new List<CNFClause>();
            cl.AddRange(a.Clauses);
            cl.AddRange(b.Clauses);

            return new CNFSet(cl);
        }

        public override string ToString()
        {
            return String.Join(" ", Clauses);
        }

        public bool Resolution()
        {
            List<CNFClause> localClauses = new List<CNFClause>(Clauses);
            do
            {
                List<CNFClause> newresolvents = new List<CNFClause>();

                for (int a = 0; a < localClauses.Count; a++)
                {
                    for (int b = a + 1; b < localClauses.Count; b++)
                    {
                        CNFClause resolvent = CNFClause.Resolve(localClauses[a], localClauses[b]);
                        if (resolvent.Atoms.Count == 0) { return true; }
                        newresolvents.Add(resolvent);
                    }
                }

                bool subset = true;
                foreach (CNFClause cl in newresolvents)
                {
                    if (!localClauses.Contains(cl))
                    {
                        subset = false;
                        localClauses.Add(cl);
                    }
                }

                if (subset) { return false; }
            } while (true);
        }
    }
}
